↳ Prolog
↳ PrologToPiTRSProof
normal_in(F, F) → normal_out(F, F)
normal_in(F, N) → U1(F, N, rewrite_in(F, F1))
rewrite_in(op(A, op(B, C)), op(A, L)) → U3(A, B, C, L, rewrite_in(op(B, C), L))
rewrite_in(op(op(A, B), C), op(A, op(B, C))) → rewrite_out(op(op(A, B), C), op(A, op(B, C)))
U3(A, B, C, L, rewrite_out(op(B, C), L)) → rewrite_out(op(A, op(B, C)), op(A, L))
U1(F, N, rewrite_out(F, F1)) → U2(F, N, normal_in(F1, N))
U2(F, N, normal_out(F1, N)) → normal_out(F, N)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
normal_in(F, F) → normal_out(F, F)
normal_in(F, N) → U1(F, N, rewrite_in(F, F1))
rewrite_in(op(A, op(B, C)), op(A, L)) → U3(A, B, C, L, rewrite_in(op(B, C), L))
rewrite_in(op(op(A, B), C), op(A, op(B, C))) → rewrite_out(op(op(A, B), C), op(A, op(B, C)))
U3(A, B, C, L, rewrite_out(op(B, C), L)) → rewrite_out(op(A, op(B, C)), op(A, L))
U1(F, N, rewrite_out(F, F1)) → U2(F, N, normal_in(F1, N))
U2(F, N, normal_out(F1, N)) → normal_out(F, N)
NORMAL_IN(F, N) → U11(F, N, rewrite_in(F, F1))
NORMAL_IN(F, N) → REWRITE_IN(F, F1)
REWRITE_IN(op(A, op(B, C)), op(A, L)) → U31(A, B, C, L, rewrite_in(op(B, C), L))
REWRITE_IN(op(A, op(B, C)), op(A, L)) → REWRITE_IN(op(B, C), L)
U11(F, N, rewrite_out(F, F1)) → U21(F, N, normal_in(F1, N))
U11(F, N, rewrite_out(F, F1)) → NORMAL_IN(F1, N)
normal_in(F, F) → normal_out(F, F)
normal_in(F, N) → U1(F, N, rewrite_in(F, F1))
rewrite_in(op(A, op(B, C)), op(A, L)) → U3(A, B, C, L, rewrite_in(op(B, C), L))
rewrite_in(op(op(A, B), C), op(A, op(B, C))) → rewrite_out(op(op(A, B), C), op(A, op(B, C)))
U3(A, B, C, L, rewrite_out(op(B, C), L)) → rewrite_out(op(A, op(B, C)), op(A, L))
U1(F, N, rewrite_out(F, F1)) → U2(F, N, normal_in(F1, N))
U2(F, N, normal_out(F1, N)) → normal_out(F, N)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
NORMAL_IN(F, N) → U11(F, N, rewrite_in(F, F1))
NORMAL_IN(F, N) → REWRITE_IN(F, F1)
REWRITE_IN(op(A, op(B, C)), op(A, L)) → U31(A, B, C, L, rewrite_in(op(B, C), L))
REWRITE_IN(op(A, op(B, C)), op(A, L)) → REWRITE_IN(op(B, C), L)
U11(F, N, rewrite_out(F, F1)) → U21(F, N, normal_in(F1, N))
U11(F, N, rewrite_out(F, F1)) → NORMAL_IN(F1, N)
normal_in(F, F) → normal_out(F, F)
normal_in(F, N) → U1(F, N, rewrite_in(F, F1))
rewrite_in(op(A, op(B, C)), op(A, L)) → U3(A, B, C, L, rewrite_in(op(B, C), L))
rewrite_in(op(op(A, B), C), op(A, op(B, C))) → rewrite_out(op(op(A, B), C), op(A, op(B, C)))
U3(A, B, C, L, rewrite_out(op(B, C), L)) → rewrite_out(op(A, op(B, C)), op(A, L))
U1(F, N, rewrite_out(F, F1)) → U2(F, N, normal_in(F1, N))
U2(F, N, normal_out(F1, N)) → normal_out(F, N)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
REWRITE_IN(op(A, op(B, C)), op(A, L)) → REWRITE_IN(op(B, C), L)
normal_in(F, F) → normal_out(F, F)
normal_in(F, N) → U1(F, N, rewrite_in(F, F1))
rewrite_in(op(A, op(B, C)), op(A, L)) → U3(A, B, C, L, rewrite_in(op(B, C), L))
rewrite_in(op(op(A, B), C), op(A, op(B, C))) → rewrite_out(op(op(A, B), C), op(A, op(B, C)))
U3(A, B, C, L, rewrite_out(op(B, C), L)) → rewrite_out(op(A, op(B, C)), op(A, L))
U1(F, N, rewrite_out(F, F1)) → U2(F, N, normal_in(F1, N))
U2(F, N, normal_out(F1, N)) → normal_out(F, N)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
REWRITE_IN(op(A, op(B, C)), op(A, L)) → REWRITE_IN(op(B, C), L)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
REWRITE_IN(op(A, op(B, C))) → REWRITE_IN(op(B, C))
From the DPs we obtained the following set of size-change graphs:
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
NORMAL_IN(F, N) → U11(F, N, rewrite_in(F, F1))
U11(F, N, rewrite_out(F, F1)) → NORMAL_IN(F1, N)
normal_in(F, F) → normal_out(F, F)
normal_in(F, N) → U1(F, N, rewrite_in(F, F1))
rewrite_in(op(A, op(B, C)), op(A, L)) → U3(A, B, C, L, rewrite_in(op(B, C), L))
rewrite_in(op(op(A, B), C), op(A, op(B, C))) → rewrite_out(op(op(A, B), C), op(A, op(B, C)))
U3(A, B, C, L, rewrite_out(op(B, C), L)) → rewrite_out(op(A, op(B, C)), op(A, L))
U1(F, N, rewrite_out(F, F1)) → U2(F, N, normal_in(F1, N))
U2(F, N, normal_out(F1, N)) → normal_out(F, N)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
NORMAL_IN(F, N) → U11(F, N, rewrite_in(F, F1))
U11(F, N, rewrite_out(F, F1)) → NORMAL_IN(F1, N)
rewrite_in(op(A, op(B, C)), op(A, L)) → U3(A, B, C, L, rewrite_in(op(B, C), L))
rewrite_in(op(op(A, B), C), op(A, op(B, C))) → rewrite_out(op(op(A, B), C), op(A, op(B, C)))
U3(A, B, C, L, rewrite_out(op(B, C), L)) → rewrite_out(op(A, op(B, C)), op(A, L))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
U11(rewrite_out(F1)) → NORMAL_IN(F1)
NORMAL_IN(F) → U11(rewrite_in(F))
rewrite_in(op(A, op(B, C))) → U3(A, rewrite_in(op(B, C)))
rewrite_in(op(op(A, B), C)) → rewrite_out(op(A, op(B, C)))
U3(A, rewrite_out(L)) → rewrite_out(op(A, L))
rewrite_in(x0)
U3(x0, x1)
U11(rewrite_out(F1)) → NORMAL_IN(F1)
NORMAL_IN(F) → U11(rewrite_in(F))
POL(NORMAL_IN(x1)) = 2 + 2·x1
POL(U11(x1)) = 2·x1
POL(U3(x1, x2)) = 2 + 2·x1 + x2
POL(op(x1, x2)) = 2 + 2·x1 + x2
POL(rewrite_in(x1)) = x1
POL(rewrite_out(x1)) = 2 + x1
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ PisEmptyProof
rewrite_in(op(A, op(B, C))) → U3(A, rewrite_in(op(B, C)))
rewrite_in(op(op(A, B), C)) → rewrite_out(op(A, op(B, C)))
U3(A, rewrite_out(L)) → rewrite_out(op(A, L))
rewrite_in(x0)
U3(x0, x1)